Nuprl Lemma : set_lt_is_sp_of_leq_a
13,42
postcript
pdf
p
:PosetSig,
a
,
b
:|
p
|. (
a
<
p
b
)
((
a
b
) & (
(
b
a
)))
latex
Up
sets
1
Definitions
strict_part(
x
,
y
.
R
(
x
;
y
);
a
;
b
)
Lemmas
set
lt
is
sp
of
leq
origin
p:PosetSig, a, b:|p|. (a <p b) 
((a 
b) & (
(b a))) p:PosetSig, a, b:|p|. (a <p b) ((a b) & ((b a)))